inl($x$) $\Rightarrow$ ${\it body}$($x$) ; ${\it cont}$(${\it value}$,${\it contvalue}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$Case ${\it value}$ of inl($x$) $\Rightarrow$ ${\it body}$($x$) ; inr($\_$) $\Rightarrow$ ${\it cont}$(${\it contvalue}$,${\it contvalue}$)